Problem:
 p(f(f(x))) -> q(f(g(x)))
 p(g(g(x))) -> q(g(f(x)))
 q(f(f(x))) -> p(f(g(x)))
 q(g(g(x))) -> p(g(f(x)))

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {4,3}
   transitions:
    p1(27) -> 28*
    g1(15) -> 16*
    g1(5) -> 6*
    g1(18) -> 19*
    f1(25) -> 26*
    f1(17) -> 18*
    f1(6) -> 7*
    q1(7) -> 8*
    p0(2) -> 3*
    p0(1) -> 3*
    f0(2) -> 1*
    f0(1) -> 1*
    q0(2) -> 4*
    q0(1) -> 4*
    g0(2) -> 2*
    g0(1) -> 2*
    1 -> 25,15
    2 -> 17,5
    7 -> 27*
    8 -> 3*
    16 -> 6*
    19 -> 7*
    26 -> 18*
    28 -> 4*
  problem:
   
  Qed